Mostly-Automated Verification of Low-Level Programs in Computational Separation LogicCHLIPALA, Adam.ACM SIGPLAN notices. 2011, Vol 46, Num 6, pp 234-245, issn 1523-2867, 12 p.Conference Paper

Parametric Higher-Order Abstract Syntax for Mechanized SemanticsCHLIPALA, Adam.ACM SIGPLAN notices. 2008, Vol 43, Num 9, pp 143-156, issn 1523-2867, 14 p.Conference Paper

Modular development of certified program verifiers with a proof assistantCHLIPALA, Adam.ACM SIGPLAN notices. 2006, Vol 41, Num 9, pp 160-171, issn 1523-2867, 12 p.Conference Paper

A framework for certified program analysis and its applications to mobile-code safetyCHANG, Bor-Yuh Evan; CHLIPALA, Adam; NECULA, George C et al.Lecture notes in computer science. 2006, pp 174-189, issn 0302-9743, isbn 3-540-31139-4, 1Vol, 16 p.Conference Paper

A Verified Compiler for an Impure Functional LanguageCHLIPALA, Adam.ACM SIGPLAN notices. 2010, Vol 45, Num 1, pp 93-106, issn 1523-2867, 14 p.Conference Paper

Ur: Statically-Typed Metaprogramming with Type-Level Record ComputationCHLIPALA, Adam.ACM SIGPLAN notices. 2010, Vol 45, Num 6, pp 122-133, issn 1523-2867, 12 p.Conference Paper

A certified type-preserving compiler from lambda calculus to assembly languageCHLIPALA, Adam.ACM SIGPLAN notices. 2007, Vol 42, Num 6, pp 54-65, issn 1523-2867, 12 p.Conference Paper

The BLAST query language for software verificationBEYER, Dirk; CHLIPALA, Adam J; HENZINGER, Thomas A et al.Lecture notes in computer science. 2004, pp 2-18, issn 0302-9743, isbn 3-540-22791-1, 17 p.Conference Paper

Effective Interactive Proofs for Higher-Order Imperative ProgramsCHLIPALA, Adam; MALECHA, Gregory; MORRISETT, Greg et al.ACM SIGPLAN notices. 2009, Vol 44, Num 9, pp 79-90, issn 1523-2867, 12 p.Conference Paper

Generating tests from counterexamplesBEYER, Dirk; CHLIPALA, Adam J; HENZINGER, Thomas A et al.International Conference on Software Engineering. 2004, pp 326-335, isbn 0-7695-2163-0, 1Vol, 10 p.Conference Paper